Inference at * 1 3 1 0 1 
Iof proof for Lemma fincr wf:

.....assertion..... NILNIL

1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. 
  zz, n:. (n < zz)  (P(n)) 

latex

 by (\p.Thin (get_int_arg `hn` p) p) 

latex

 1: 

 1: 2. j:. (k:. (k < j)  (P(k)))  (P(j))
 1:   zz, n:. (n < zz)  (P(n))
 .

Definitions

f(a), a < b, P  Q, x:A. B(x), , , x:AB(x)